1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
use super::*;
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct NormalCfg {
pub max_steps: u64,
pub eta: bool,
pub head: bool,
pub sub: bool,
}
impl NormalCfg {
pub fn to_form(form: Form, max_steps: u64) -> NormalCfg {
NormalCfg {
max_steps,
eta: form.is_enf(),
head: form.is_hnf(),
sub: form.is_bnf() || form.is_enf(),
}
}
}
impl ReductionConfig for NormalCfg {
type AsRef = NormalCfg;
#[inline]
fn register_push_subst(&mut self, _subst: &TermId) -> Result<(), Error> {
Ok(())
}
#[inline]
fn register_pop_subst(&mut self) -> Result<(), Error> {
Ok(())
}
#[inline]
fn register_beta(&mut self) -> Result<(), Error> {
if self.max_steps == 0 {
return Err(Error::StopReduction);
}
self.max_steps -= 1;
Ok(())
}
#[inline]
fn register_eta(&mut self) -> Result<(), Error> {
if self.max_steps == 0 {
return Err(Error::StopReduction);
}
self.max_steps -= 1;
Ok(())
}
#[inline]
fn eta(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.max_steps == 0 {
return Err(Error::StopReduction);
} else {
Ok(self.eta)
}
}
#[inline]
fn sub(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.max_steps == 0 {
return Err(Error::StopReduction);
} else {
Ok(self.sub)
}
}
#[inline]
fn head(&self, _term: &Term, _ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.max_steps == 0 {
return Err(Error::StopReduction);
} else {
Ok(self.head)
}
}
#[inline]
fn intersects(&self, _filter: VarFilter, _code: Code, form: Form) -> bool {
(self.head && !form.is_hnf())
|| (self.sub && !((self.head && form.is_bnf()) && (self.eta && form.is_enf())))
|| (self.eta && !form.is_enf())
}
#[inline]
fn as_ref_mut(&mut self) -> &mut Self::AsRef {
self
}
}